

Checking transition consistency


msc diagrams: three_way_connect(18) and CW_answer(9)
INCONSISTENCY:
Matching formula: k18 = k9
Precondition 1: rel (m18 , k18 , connected) & rel (k18 , n18 , three_wayhold); Precondition 2: state (n9 , ringing k9) & rel (k9 , m9 , connected);
Post condition 1: rel (m18 , n18 , three_wayconnected k18); Post condition 2: rel (k9 , m9 , cw hold connect n9);

msc diagrams: three_way_initial(15) and CW_answer(9)
INCONSISTENCY:
Matching formula: m15 = k9
Precondition 1: rel (m15 , n15 , connected) & Forall k (~(rel (m15 , k , three_wayhold))); Precondition 2: state (n9 , ringing k9) & rel (k9 , m9 , connected);
Post condition 1: state (m15 , dial) & rel (m15 , n15 , three_wayhold); Post condition 2: rel (k9 , m9 , cw hold connect n9);

msc diagrams: three_way_teardown1(14) and three_way_teardown2(11)
INCONSISTENCY:
Matching formula: m14 = k11
Precondition 1: rel (m14 , n14 , three_wayconnected k14); Precondition 2: rel (m11 , n11 , three_wayconnected k11);
Post condition 1: rel (n14 , k14 , connected); Post condition 2: state (m11 , dial) & state (n11 , dial);

msc diagrams: three_way_teardown1(14) and CW_teardown1(6)
INCONSISTENCY:
Matching formula: m14 = m6
Precondition 1: rel (m14 , n14 , three_wayconnected k14); Precondition 2: rel (k6 , n6 , cw hold connect m6);
Post condition 1: rel (n14 , k14 , connected); Post condition 2: rel (k6 , n6 , connected);

msc diagrams: three_way_teardown1(14) and CW_teardown2(4)
INCONSISTENCY:
Matching formula: m14 = m4
Precondition 1: rel (m14 , n14 , three_wayconnected k14); Precondition 2: rel (k4 , m4 , cw hold connect n4);
Post condition 1: rel (n14 , k14 , connected); Post condition 2: rel (k4 , n4 , cw hold);

msc diagrams: three_way_teardown1(14) and CW_teardown3(1)
INCONSISTENCY:
Matching formula: m14 = k1
Precondition 1: rel (m14 , n14 , three_wayconnected k14); Precondition 2: rel (k1 , n1 , cw hold connect m1);
Post condition 1: rel (n14 , k14 , connected); Post condition 2: state (m1 , diale) & state (n1 , diale);

msc diagrams: three_way_teardown2(11) and CW_teardown1(6)
INCONSISTENCY:
Matching formula: k11 = m6
Precondition 1: rel (m11 , n11 , three_wayconnected k11); Precondition 2: rel (k6 , n6 , cw hold connect m6);
Post condition 1: state (m11 , dial) & state (n11 , dial); Post condition 2: rel (k6 , n6 , connected);

msc diagrams: three_way_teardown2(11) and CW_teardown2(4)
INCONSISTENCY:
Matching formula: k11 = m4
Precondition 1: rel (m11 , n11 , three_wayconnected k11); Precondition 2: rel (k4 , m4 , cw hold connect n4);
Post condition 1: state (m11 , dial) & state (n11 , dial); Post condition 2: rel (k4 , n4 , cw hold);

msc diagrams: three_way_teardown2(11) and CW_teardown3(1)
INCONSISTENCY:
Matching formula: k11 = k1
Precondition 1: rel (m11 , n11 , three_wayconnected k11); Precondition 2: rel (k1 , n1 , cw hold connect m1);
Post condition 1: state (m11 , dial) & state (n11 , dial); Post condition 2: state (m1 , diale) & state (n1 , diale);

msc diagrams: three_way_teardown3(10) and CW_switch2(7)
INCONSISTENCY:
Matching formula: m10 = k7
Precondition 1: state (m10 , dial) & rel (m10 , n10 , three_wayhold); Precondition 2: rel (k7 , m7 , cw hold);
Post condition 1: rel (m10 , n10 , connected); Post condition 2: rel (k7 , m7 , connected);